Weak MSO+U with Path Quantifiers over Infinite Trees

摘要

This paper shows that over infinite trees, satisfiability is decidable forweak monadic second-order logic extended by the unbounding quantifier U andquantification over infinite paths. The proof is by reduction to emptiness fora certain automaton model, while emptiness for the automaton model is decidedusing profinite trees.